package karpiel.boguchwal.wojciech.przemek

import java.io.{Reader, StringReader}

import karpiel.boguchwal.wojciech.przemek.Ast._
import karpiel.boguchwal.wojciech.przemek.NoDepsParser.ParseException
import karpiel.boguchwal.wojciech.przemek.TokenTree.{Atom, Lst}

import scala.collection.mutable
import scala.collection.mutable.ListBuffer

object NoDepsParser {

  class ParseException(msg: String) extends PrzemekException(msg)

  case class Output(initalContext: Context, expression: Ast)(implicit cache: Cache) {
    lazy val bruinizedExpr: Ast = Bruinizer.bruinize(expression)(initalContext, implicitly)
  }

  def parse(reader: CharReader)(implicit cache: Cache) = {
    val tokenTrees = new TokenTreeBuilder(new Lexer(new PeekingReader(() => reader.readChar())).tokens).result
    val initDecls: Seq[TokenTree] = tokenTrees.take(tokenTrees.size - 1)
    val valDecls: Seq[ValueDeclarationsHandler.ValDecl] = initDecls.map {
      case Lst(Seq(Atom("set"), Atom(name), valueTree)) => ValueDeclarationsHandler.ValDeclN(name, AltAstBuilder.buildAst(valueTree))
      case Lst(Seq(Atom("set"), Atom(name), typeTree, valueTree)) =>
        ValueDeclarationsHandler.ValDeclT(name, AltAstBuilder.buildAst(typeTree), AltAstBuilder.buildAst(valueTree))
      case q => throw new ParseException(q.toString)
    }

    val ctx = ValueDeclarationsHandler.prepareContext(valDecls.toList)
    val expression = tokenTrees.last
    val expressionAst = AltAstBuilder.buildAst(expression)
    Output(ctx, expressionAst)
  }

  def parse(string: String)(implicit cache: Cache): Output = parse(new StringReader(string))

  def parse(reader: Reader)(implicit cache: Cache): Output = parse(() => Some(reader.read()).filterNot(_ == -1).map(_.asInstanceOf[Char]))
}

trait CharReader {
  /**
    * @return Some(c) until EOF, then None
    */
  def readChar(): Option[Char]
}

object AltAstBuilder {
  def buildAst(tokenTree: TokenTree): Ast = {
    tokenTree match {
      case Atom(s) => s match {
        case "true" => BoolTrue
        case "false" => BoolFalse
        case "Bool" => BoolType
        case "Unit" => UnitType
        case "Empty" => EmptyType
        case "tt" => UnitValue
        case varName =>
          Var(varName)
      }
      //      case Lst(Seq(Atom("lambda"), Lst(Seq(Atom(varl), typ)), c)) => PiValue(NamedType(varl, buildAst(typ)), buildAst(c))
      //      case Lst(Seq(Atom("Pi"), Lst(Seq(Atom(varl), typ)), c)) => PiType(NamedType(varl, buildAst(typ)), buildAst(c))
      case Lst(sq) if piConvinienceGuard("lambda", sq) => piElo(sq)
      case Lst(sq) if piConvinienceGuard("Pi", sq) => piElo(sq)
      case Lst(Seq(Atom("Universe"), Atom(x))) => Universe(x.toInt)
      case Lst(Seq(Atom("Bruijn"), Atom(x))) => Bruijn(x.toInt, Option.empty)
      case Lst(Seq(Atom("sum"), a, b)) => SumType(a.toAst, b.toAst)
      case Lst(Seq(Atom("inl"), a, b)) => SumInl(a.toAst, b.toAst)
      case Lst(Seq(Atom("inr"), a, b)) => SumInr(a.toAst, b.toAst)
      case Lst(Seq(Atom("sumElim"), a, b)) => SumElim(a.toAst, b.toAst)
      case Lst(Seq(Atom("Bool-ind"), a, b)) => BoolElim(a.toAst, b.toAst)
      case Lst(Seq(Atom("Bool-rec"), q, a, b)) => Ast.BoolRec(q.toAst, a.toAst, b.toAst)
      case Lst(Seq(Atom("Empty-ind"), a)) => EmptyElim(a.toAst)
      case Lst(Seq(Atom("W"), a)) => Ast.WType(a.toAst)
      case Lst(Seq(Atom("W-rec"), a, b)) => WElim(a.toAst, b.toAst)
      case Lst(Seq(Atom("WSup"), a, b, c)) => WSup(a.toAst, b.toAst, c.toAst)
      case Lst(Seq(Atom("Id"), a, b)) => IdType(a.toAst, b.toAst)
      case Lst(Seq(Atom("refl"), a)) => Refl(a.toAst)
      case Lst(Seq(Atom("J"), a, b)) => J(a.toAst, b.toAst)
      case Lst(Seq(a, b)) => PiElim(a.toAst, b.toAst)
      //todo dla wygody ale niebezpieczne
      case Lst(sq) if sq.nonEmpty => sq.map(_.toAst).reduce((t, q) => PiElim(t, q))

      case q => throw new ParseException(q.toString)
    }
  }

  def piConvinienceGuard(reqAtom: String, sq: Seq[TokenTree]): Boolean = {
    sq.size >= 3 &&
      sq.head == Atom(reqAtom) && {
      val last = sq.last
      val nameDefs_ = sq.tail.take(sq.size - 2)
      nameDefs_.forall {
        case Lst(Seq(Atom(varl), typ)) => true
        case _ => false
      }

    }
  }

  def piElo(sq: Seq[TokenTree]) = {
    val fnBody = sq.last.toAst
    val nameDefs_ = sq.tail.take(sq.size - 2)
    val nameDefs = nameDefs_.map {
      case Lst(Seq(Atom(varl), typ)) => NamedType(varl, typ.toAst)
      case _ => throw new PrzemekException("DDD")
    }
    val fn = if (sq.head.asInstanceOf[Atom].s == "Pi") (a: Ast, b: Ast) => PiType(a, b)
    else if (sq.head.asInstanceOf[Atom].s == "lambda") (a: Ast, b: Ast) => PiValue(a, b)
    else throw new PrzemekException("dweqfewfwegr")

    nameDefs.foldRight(fnBody)((nt, fnB) => fn(nt, fnB))
  }

  private def convinience(s: List[TokenTree]): Ast = {
    s match {
      case last :: Nil => last.toAst
      case h :: t => PiElim(h.toAst, convinience(t))
      case Nil => throw new PrzemekException("TAK NIE MOŻE BYĆ!!!!")
    }
  }

  implicit class TTUtil(t: TokenTree) {
    def toAst: Ast = buildAst(t)
  }

}

trait MyReader {
  def consume(): Option[Char]

  def peek(): Option[Char]
}

class PeekingReader(consumeChar: () => Option[Char]) extends MyReader {
  var peeked: Option[Char] = Option.empty

  override def consume(): Option[Char] = {
    updatePeek()
    val p = peeked
    peeked = Option.empty
    p
  }

  override def peek(): Option[Char] = {
    updatePeek()
    peeked
  }

  private def updatePeek(): Unit = if (peeked.isEmpty) peeked = consumeChar()
}

class Lexer(reader: MyReader) {
  val tokens = new mutable.ListBuffer[String]()

  private def readToken(acc: String = ""): String = reader.peek() match {
    case Some('(') | Some(')') | Some('\n') | Some(' ') | Some('\t') | None => acc
    case Some(_) => readToken(acc + reader.consume().get)
  }

  private def read(): Unit = {
    reader.peek() match {
      case Some('(') | Some(')') => tokens += reader.consume().get + ""
        read()
      case Some('\n') | Some(' ') | Some('\t') => reader.consume()
        read()
      case Some(';') => ignoreUntilNextLine()
        read()
      case Some(legitChar) => tokens += readToken()
        read()
      case None =>
    }
  }

  private def ignoreUntilNextLine(): Unit = {
    reader.peek() match {
      case Some('\n') => reader.consume()
      case Some(_) => reader.consume()
        ignoreUntilNextLine()
      case None =>
    }
  }

  {
    read()
  }
}

sealed trait TokenTree

object TokenTree {

  case class Atom(s: String) extends TokenTree

  case class Lst(var inner: Seq[TokenTree]) extends TokenTree

}


class TokenTreeBuilder(tokens: ListBuffer[String]) {
  private val it = tokens.iterator
  private var listStack = List[Lst](Lst(Seq())) //strażnik


  private def doq(): Unit = {
    while (it.hasNext) {
      val n = it.next()
      n match {
        case ")" => listStack = listStack.tail
        case "(" =>
          val newList = Lst(Seq())
          listStack.head.inner = listStack.head.inner ++ Seq(newList)
          listStack = newList :: listStack
        case atom => listStack.head.inner = listStack.head.inner ++ Seq(Atom(atom))
      }
    }
  }

  doq()
  if (listStack.size != 1) throw new ParseException(listStack.size + "")
  val result: Seq[TokenTree] = listStack.head.inner
}

